$\forall$$T$:Type, $P$:($T$$\rightarrow$Prop).
\\[0ex]($\forall$$x$:$T$. Dec($P$($x$))) $\Rightarrow$ (finite{-}type(\{$x$:$T$$\mid$ $P$($x$) \}) $\Leftrightarrow$ ($\exists$$L$:$T$ List. $\forall$$x$:$T$. $P$($x$) $\Rightarrow$ ($x$ $\in$ $L$)))